$\forall$$T$:Type, ${\it as}$,${\it bs}$:($T$ List), $a$,$b$:$T$. \\[0ex]compat($T$; cons($a$; ${\it as}$); cons($b$; ${\it bs}$)) $\Leftarrow\!\Rightarrow$ (($a$ = $b$) $\wedge$ compat($T$; ${\it as}$; ${\it bs}$))